Nuprl Lemma : map_is_nil
11,40
postcript
pdf
A
,
B
:Type,
f
:(
A
B
),
l
:(
A
List). (map(
f
;
l
) = []
(
B
List))
(
l
= [])
latex
Definitions
Y
,
map(
f
;
as
)
,
t
T
,
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
&
Q
,
P
Q
,
False
Lemmas
map
wf
origin
A, B:Type, f:(A
B), l:(A List). (map(f;l) = [] 
(B List)) 
(l = []) A, B:Type, f:(AB), l:(A List). (map(f;l) = [] (B List)) (l = []) T
Qx:A. B(x) Q Q